T:Type, a,x:T. (x  cons(a; []))  (x = a) 

latex

Definitions	False, A, A  B, prop{i:l}, t  T, P  Q, P  Q, P  Q, Y, ||as||, A c B, x:A. B(x), (x  l), P  Q, x:A. B(x), ff, tt, i <z j, b, i z j, if b then t else f fi , nth_tl(n;as), hd(l), l[i], , guard(T), sq_type(T), P  Q, decidable(P)
Lemmas	select wf, nat wf, length wf1, neg assert of eq int, nat sq, le wf, assert of eq int, eq int wf, decidable assert